#include <stdlib.h>
#include <stdio.h>
#include "Parallelizer.cuh"

__global__ void run_parallel(DataToDevice data)
{

	int index = threadIdx.x + blockIdx.x * blockDim.x;

#ifdef ENABLE_STATISTICS
	data.get_statistics().signal_create_structures_start();
#endif

#ifdef ASSUMPTIONS_USE_DYNAMICALLY_ALLOCATED_VECTOR
	GPUVec<Lit>* assumptions = (data.get_all_assumptions_parallel()).get_ptr(index);
#else
	GPUStaticVec<Lit> the_assumptions;
	GPUStaticVec<Lit> * assumptions = (&the_assumptions);
#endif

	JobsQueue queue = data.get_jobs_queue();

	int largest_job_size = queue.largest_job_size();

	CUDAClauseVec clause_db = data.get_clauses_db();
	int number_of_variables = data.get_number_of_variables();
	int max_implications_per_var = data.get_max_implication_per_var();
	GPUVec<Var> dead_vars = data.get_dead_vars();
	//GPUVec <WatchedClause> watched_clauses = data.get_watched_clauses(index);

	SATSolver solver(
			clause_db,
			number_of_variables,
			max_implications_per_var,
			dead_vars,
#ifdef ENABLE_STATISTICS
			&(data.get_statistics()),
#endif
			data.get_nodes_repository_ptr()
			//,watched_clauses
			);

	sat_status status = UNSAT;

#ifdef ENABLE_STATISTICS
	data.get_statistics().signal_create_structures_stop();
#endif

#ifdef ENABLE_STATISTICS
	data.get_statistics().signal_next_job_start();
#endif
	Job job = queue.next_job();
#ifdef ENABLE_STATISTICS
	data.get_statistics().signal_next_job_stop();
#endif

#ifdef DEBUG
	if(DEBUG_SHOULD_PRINT(threadIdx.x, blockIdx.x))
	{
		printf("Block: %d, thread: %d, index: %d\n", blockIdx.x, threadIdx.x, index );
		printf("Largest job is : %d\n", largest_job_size);
		printf("Number of literals: %d\n", job.number_of_literals);
	}
#endif


	int solved_jobs = 0;

	while(job.number_of_literals > 0)
	{

#ifdef ENABLE_STATISTICS
	data.get_statistics().signal_job_start();
#endif
		solved_jobs++;

#ifdef DEBUG
		if(DEBUG_SHOULD_PRINT(threadIdx.x, blockIdx.x))
		{
			printf("Thread of index %d is running job: ", index);
			print_job(job);
			printf("\n");
		}
#endif

#ifdef ENABLE_STATISTICS
	data.get_statistics().signal_add_jobs_to_assumptions_start();
#endif
		for(int i = 0; i < job.number_of_literals; i++)
		{
			assumptions->add(job.literals[i]);
		}

#ifdef ENABLE_STATISTICS
	data.get_statistics().signal_add_jobs_to_assumptions_stop();
#endif



#ifdef DEBUG
	if(DEBUG_SHOULD_PRINT(threadIdx.x, blockIdx.x))
	{
		printf("The jobs as assumptions are: ");
		for(int i = 0; i < assumptions->size_of(); i++)
		{
			print_lit(assumptions->get(i));
			printf(" ");
		}
		printf("\n");
	}
#endif

		status = solver.solve(assumptions);

#ifdef ENABLE_STATISTICS
		data.get_statistics().signal_job_stop();
#endif

		if(status == SAT || status == UNDEF)
		{
			break;
		}

#ifdef ENABLE_STATISTICS
		data.get_statistics().signal_reset_structures_start();
#endif

		solver.reset();

#ifdef ENABLE_STATISTICS
		data.get_statistics().signal_reset_structures_stop();
#endif

#ifdef ENABLE_STATISTICS
	data.get_statistics().signal_add_jobs_to_assumptions_start();
#endif
		assumptions->remove_n_last(job.number_of_literals);

#ifdef ENABLE_STATISTICS
	data.get_statistics().signal_add_jobs_to_assumptions_stop();
#endif

#ifdef ENABLE_STATISTICS
	data.get_statistics().signal_next_job_start();
#endif
		job = queue.next_job();
#ifdef ENABLE_STATISTICS
	data.get_statistics().signal_next_job_stop();
#endif


	}
#ifdef ENABLE_STATISTICS
	data.get_statistics().add_completed_jobs(solved_jobs);
#endif

#ifdef DEBUG
	if(DEBUG_SHOULD_PRINT(threadIdx.x, blockIdx.x))
	{
		printf("End of loop.\n");
	}
#endif

#ifdef ENABLE_STATISTICS
	data.get_statistics().signal_process_results_start();
#endif
	if(status == SAT)
	{
		//printf("Size of assumptions = %d\n", all_assumptions.size_of());
		// TODO replace 1000 for something else.
		int first = atomicInc(data.get_found_answer_ptr(), 1000);

		if(first == 0)
		{
			int results_size = solver.get_results_size();

			Lit* the_results = (Lit*) malloc(results_size*sizeof(Lit));

			Results results = data.get_results();

			solver.get_results(the_results);

			results.set_satisfiable_results(the_results, results_size);

			free(the_results);

		}
	}

	if(status == UNSAT)
	{
		syncthreads();
	}
	if(status == UNDEF)
	{
		Results results = data.get_results();
		int first = atomicInc(data.get_found_answer_ptr(), 1000);
		printf("Block %d, thread %d had a problem\n", blockIdx.x, threadIdx.x);
		results.set_undef();
	}

#ifdef ENABLE_STATISTICS
	data.get_statistics().signal_process_results_stop();
#endif


}


__global__ void run_sequential(DataToDevice data)
{
#ifdef ENABLE_STATISTICS
	data.get_statistics().signal_create_structures_start();
#endif

	CUDAClauseVec clauses_db = data.get_clauses_db();
	int number_of_variables = data.get_number_of_variables();

#ifdef ASSUMPTIONS_USE_DYNAMICALLY_ALLOCATED_VECTOR
		GPUVec<Lit> assumptions = data.get_assumptions_sequential();
#else
		//GPUStaticVec<Lit> assumptions = data.get_assumptions_sequential();
#endif

	Results  results = data.get_results();
	int max_implication_per_var = data.get_max_implication_per_var();
	GPUVec <Var> dead_vars = data.get_dead_vars();

	//GPUVec <WatchedClause> watched_clauses = data.get_watched_clauses(0);

	SATSolver solver(clauses_db, number_of_variables, max_implication_per_var,
			dead_vars,
#ifdef ENABLE_STATISTICS
			data.get_statistics_ptr(),
#endif
			data.get_nodes_repository_ptr()
			//, watched_clauses
			);

#ifdef ENABLE_STATISTICS
	data.get_statistics().signal_create_structures_stop();
#endif
#ifdef ENABLE_STATISTICS
	data.get_statistics_ptr()->signal_job_start();
#endif

#ifdef ASSUMPTIONS_USE_DYNAMICALLY_ALLOCATED_VECTOR
	sat_status status = solver.solve(&assumptions);
#else
	sat_status status = solver.solve();
#endif

#ifdef ENABLE_STATISTICS
	data.get_statistics_ptr()->signal_job_stop();
#endif

#ifdef ENABLE_STATISTICS
	data.get_statistics().signal_process_results_start();
#endif

	if(status == SAT)
	{
		int results_size = solver.get_results_size();

		Lit* the_results = (Lit*) malloc(results_size*sizeof(Lit));

		solver.get_results(the_results);

		results.set_satisfiable_results(the_results, results_size);

		free(the_results);
	}
	if(status == UNSAT)
	{
		// do nothing!
	}
	if(status == UNDEF)
	{
		results.set_undef();
	}

#ifdef ENABLE_STATISTICS
	data.get_statistics().signal_process_results_stop();
#endif

}

